/-
Copyright (c) 2025 Monica Omar. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Monica Omar
-/
import Mathlib.Algebra.Group.Submonoid.Operations
import Mathlib.Data.Fintype.Basic

/-!
# Submonoids

This file provides some results on multiplicative and additive submonoids in the finite context.
-/

namespace Submonoid

section Pi
variable {η : Type*} {f : η → Type*} [∀ i, MulOneClass (f i)]
variable {S : Type*} [SetLike S (Π i, f i)] [SubmonoidClass S (Π i, f i)]

open Set

@[to_additive]
theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : S} (x : Π i, f i)
    (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) : x ∈ H := by
  induction I using Finset.induction_on generalizing x with
  | empty =>
    have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
    exact this ▸ one_mem H
  | insert i I hnotMem ih =>
    have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by
      ext j
      by_cases heq : j = i
      · subst heq
        simp
      · simp [heq]
    rw [this]
    clear this
    apply mul_mem (ih _ _ _) (by simp [h2]) <;> clear ih <;> intro j hj
    · by_cases heq : j = i
      · subst heq
        simp
      · simpa [heq] using h1 j (by simpa [heq] using hj)
    · have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)

@[to_additive]
theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : S} (x : Π i, f i)
    (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H := by
  cases nonempty_fintype η
  exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

/-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the monoids. -/
@[to_additive /-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the
additive monoids. -/]
theorem pi_le_iff [Finite η] [DecidableEq η] {H : Π i, Submonoid (f i)} {J : Submonoid (Π i, f i)} :
    pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J :=
  ⟨fun h i _ ⟨x, hx, H⟩ => h <| by simpa [← H],
   fun h x hx => pi_mem_of_mulSingle_mem x fun i => h i (mem_map_of_mem _ (hx i trivial))⟩

@[to_additive]
theorem closure_pi [Finite η] {s : Π i, Set (f i)} (hs : ∀ i, 1 ∈ s i) :
    closure (univ.pi fun i => s i) = pi univ fun i => closure (s i) :=
  le_antisymm
    (closure_le.2 <| pi_subset_pi_iff.2 <| .inl fun _ _ => subset_closure)
    (by
      classical
      exact pi_le_iff.mpr fun i => map_le_of_le_comap _ <| closure_le.2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _)

end Pi

end Submonoid
